Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 QTRSRRRProof (⇔)
↳2 QTRS
↳3 QTRSRRRProof (⇔)
↳4 QTRS
↳5 QTRSRRRProof (⇔)
↳6 QTRS
↳7 QTRSRRRProof (⇔)
↳8 QTRS
↳9 QTRSRRRProof (⇔)
↳10 QTRS
↳11 DependencyPairsProof (⇔)
↳12 QDP
↳13 DependencyGraphProof (⇔)
↳14 AND
    ↳15 QDP
        ↳16 UsableRulesReductionPairsProof (⇔)
        ↳17 QDP
        ↳18 MRRProof (⇔)
        ↳19 QDP
        ↳20 DependencyGraphProof (⇔)
        ↳21 AND
            ↳22 QDP
                ↳23 UsableRulesProof (⇔)
                ↳24 QDP
                ↳25 QDPSizeChangeProof (⇔)
                ↳26 YES
            ↳27 QDP
                ↳28 QDPOrderProof (⇔)
                ↳29 QDP
                ↳30 PisEmptyProof (⇔)
                ↳31 YES
            ↳32 QDP
                ↳33 Narrowing (⇔)
                ↳34 QDP
                ↳35 Narrowing (⇔)
                ↳36 QDP
                ↳37 Narrowing (⇔)
                ↳38 QDP
                ↳39 DependencyGraphProof (⇔)
                ↳40 QDP
                ↳41 Narrowing (⇔)
                ↳42 QDP
                ↳43 DependencyGraphProof (⇔)
                ↳44 QDP
                ↳45 Narrowing (⇔)
                ↳46 QDP
                ↳47 Narrowing (⇔)
                ↳48 QDP
                ↳49 DependencyGraphProof (⇔)
                ↳50 QDP
                ↳51 Narrowing (⇔)
                ↳52 QDP
                ↳53 DependencyGraphProof (⇔)
                ↳54 QDP
                ↳55 Narrowing (⇔)
                ↳56 QDP
                ↳57 DependencyGraphProof (⇔)
                ↳58 QDP
                ↳59 Narrowing (⇔)
                ↳60 QDP
                ↳61 Narrowing (⇔)
                ↳62 QDP
                ↳63 DependencyGraphProof (⇔)
                ↳64 QDP
                ↳65 Narrowing (⇔)
                ↳66 QDP
                ↳67 DependencyGraphProof (⇔)
                ↳68 QDP
                ↳69 Narrowing (⇔)
                ↳70 QDP
                ↳71 MRRProof (⇔)
                ↳72 QDP
                ↳73 MRRProof (⇔)
                ↳74 QDP
                ↳75 QDPOrderProof (⇔)
                ↳76 QDP
                ↳77 QDPOrderProof (⇔)
                ↳78 QDP
                ↳79 QDPOrderProof (⇔)
                ↳80 QDP
                ↳81 NonTerminationProof (⇔)
                ↳82 NO
            ↳83 QDP
                ↳84 QDPOrderProof (⇔)
                ↳85 QDP
                ↳86 DependencyGraphProof (⇔)
                ↳87 TRUE
    ↳88 QDP
        ↳89 UsableRulesReductionPairsProof (⇔)
        ↳90 QDP
        ↳91 Narrowing (⇔)
        ↳92 QDP
        ↳93 Narrowing (⇔)
        ↳94 QDP
        ↳95 Narrowing (⇔)
        ↳96 QDP
        ↳97 DependencyGraphProof (⇔)
        ↳98 QDP
        ↳99 Narrowing (⇔)
        ↳100 QDP
        ↳101 DependencyGraphProof (⇔)
        ↳102 QDP
        ↳103 Narrowing (⇔)
        ↳104 QDP
        ↳105 Narrowing (⇔)
        ↳106 QDP
        ↳107 DependencyGraphProof (⇔)
        ↳108 QDP
        ↳109 Narrowing (⇔)
        ↳110 QDP
        ↳111 DependencyGraphProof (⇔)
        ↳112 QDP
        ↳113 Narrowing (⇔)
        ↳114 QDP
        ↳115 DependencyGraphProof (⇔)
        ↳116 QDP
        ↳117 Narrowing (⇔)
        ↳118 QDP
        ↳119 Narrowing (⇔)
        ↳120 QDP
        ↳121 DependencyGraphProof (⇔)
        ↳122 QDP
        ↳123 Narrowing (⇔)
        ↳124 QDP
        ↳125 DependencyGraphProof (⇔)
        ↳126 QDP
        ↳127 Narrowing (⇔)
        ↳128 QDP
        ↳129 MRRProof (⇔)
        ↳130 QDP
        ↳131 MRRProof (⇔)
        ↳132 QDP
        ↳133 QDPOrderProof (⇔)
        ↳134 QDP
        ↳135 QDPOrderProof (⇔)
        ↳136 QDP
        ↳137 QDPOrderProof (⇔)
        ↳138 QDP
        ↳139 NonTerminationProof (⇔)
        ↳140 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(nil) → 0
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = x1 + 2·x2   
POL(U42(x1)) = 2·x1   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = 2·x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2·x1   
POL(n__nil) = 1   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNatList(n__nil) → tt
length(nil) → 0


(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt) → tt
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = 1 + x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 2·x1 + 2·x2   
POL(U42(x1)) = 2·x1   
POL(U51(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U11(tt) → tt


(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = x1   
POL(U41(x1, x2)) = 1 + 2·x1 + x2   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = x1 + x2 + 2·x3   
POL(U62(x1, x2)) = 2·x1 + x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = 1 + x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNatIList(V) → U31(isNatList(activate(V)))
isNatIList(n__zeros) → tt


(6) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U31(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = x1   
POL(U21(x1)) = x1   
POL(U31(x1)) = 1 + x1   
POL(U41(x1, x2)) = x1 + 2·x2   
POL(U42(x1)) = 2·x1   
POL(U51(x1, x2)) = x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U31(tt) → tt


(8) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__length(V1)) → U11(isNatList(activate(V1)))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(9) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U11(x1)) = 1 + x1   
POL(U21(x1)) = x1   
POL(U41(x1, x2)) = 2·x1 + 2·x2   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = 2·x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatIList(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

isNat(n__length(V1)) → U11(isNatList(activate(V1)))


(10) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.

(11) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZEROS → CONS(0, n__zeros)
ZEROS → 01
U411(tt, V2) → U421(isNatIList(activate(V2)))
U411(tt, V2) → ISNATILIST(activate(V2))
U411(tt, V2) → ACTIVATE(V2)
U511(tt, V2) → U521(isNatList(activate(V2)))
U511(tt, V2) → ISNATLIST(activate(V2))
U511(tt, V2) → ACTIVATE(V2)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)
U621(tt, L) → S(length(activate(L)))
U621(tt, L) → LENGTH(activate(L))
U621(tt, L) → ACTIVATE(L)
ISNAT(n__s(V1)) → U211(isNat(activate(V1)))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
LENGTH(cons(N, L)) → ACTIVATE(L)
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__0) → 01
ACTIVATE(n__length(X)) → LENGTH(activate(X))
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__nil) → NIL

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 15 less nodes.

(14) Complex Obligation (AND)

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__length(X)) → LENGTH(activate(X))
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
U511(tt, V2) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U621(tt, L) → ACTIVATE(L)
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x1)) = x1   
POL(ISNAT(x1)) = x1   
POL(ISNATLIST(x1)) = 2·x1   
POL(LENGTH(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = 2·x1 + 2·x2   
POL(U511(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3   
POL(U611(x1, x2, x3)) = 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 2·x1 + 2·x2   
POL(U621(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__length(X)) → LENGTH(activate(X))
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
U511(tt, V2) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U621(tt, L) → ACTIVATE(L)
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ACTIVATE(n__length(X)) → LENGTH(activate(X))
ACTIVATE(n__length(X)) → ACTIVATE(X)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x1)) = x1   
POL(ISNAT(x1)) = 2·x1   
POL(ISNATLIST(x1)) = 2·x1   
POL(LENGTH(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U511(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3   
POL(U611(x1, x2, x3)) = x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(U621(x1, x2)) = x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = 2·x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)
U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
U511(tt, V2) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U621(tt, L) → ACTIVATE(L)
U611(tt, L, N) → ISNAT(activate(N))
U611(tt, L, N) → ACTIVATE(N)
U611(tt, L, N) → ACTIVATE(L)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(20) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 4 SCCs with 11 less nodes.

(21) Complex Obligation (AND)

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__s(X)) → ACTIVATE(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
    The graph contains the following edges 1 > 1

  • ACTIVATE(n__s(X)) → ACTIVATE(X)
    The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNAT(n__s(V1)) → ISNAT(activate(V1))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(28) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNAT(n__s(V1)) → ISNAT(activate(V1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( ISNAT(x1) ) = max{0, 2x1 - 2}


POL( activate(x1) ) = 2x1 + 1


POL( n__zeros ) = 0


POL( zeros ) = 1


POL( n__0 ) = 0


POL( 0 ) = 0


POL( n__length(x1) ) = 0


POL( length(x1) ) = 0


POL( n__s(x1) ) = 2x1 + 2


POL( s(x1) ) = 2x1 + 2


POL( n__cons(x1, x2) ) = 0


POL( cons(x1, x2) ) = max{0, -2}


POL( n__nil ) = 0


POL( nil ) = 1


POL( U61(x1, ..., x3) ) = 2x1


POL( isNatList(x1) ) = max{0, -2}


POL( U51(x1, x2) ) = max{0, -2}


POL( isNat(x1) ) = max{0, 2x1 - 2}


POL( U21(x1) ) = 2


POL( U62(x1, x2) ) = 2


POL( tt ) = 1


POL( U52(x1) ) = max{0, 2x1 - 1}



The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
s(X) → n__s(X)
length(X) → n__length(X)
cons(X1, X2) → n__cons(X1, X2)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
zeros → n__zeros
0 → n__0
nil → n__nil

(29) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(30) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(31) YES

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, V2) → ISNATLIST(activate(V2))
ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(33) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, V2) → ISNATLIST(activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(zeros)
U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2))
U511(tt, n__zeros) → ISNATLIST(zeros)
U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(35) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(V1, V2)) → U511(isNat(activate(V1)), activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))

(36) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__zeros) → ISNATLIST(zeros)
U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(37) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__zeros) → ISNATLIST(zeros) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(n__zeros)

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__0) → ISNATLIST(0)
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, n__nil) → ISNATLIST(nil)
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(n__zeros)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(39) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1))
U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(41) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__zeros, y1)) → U511(isNat(zeros), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__zeros), activate(y0))

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__zeros), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(43) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1))
U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(45) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__0, y1)) → U511(isNat(0), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__0) → ISNATLIST(0)
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(47) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__0) → ISNATLIST(0) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__0) → ISNATLIST(n__0)

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__0) → ISNATLIST(n__0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(49) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(50) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__nil) → ISNATLIST(nil)
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(51) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__nil) → ISNATLIST(nil) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__nil) → ISNATLIST(n__nil)

(52) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__nil) → ISNATLIST(n__nil)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(53) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(55) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__nil, y1)) → U511(isNat(nil), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__nil, y0)) → U511(isNat(n__nil), activate(y0))

(56) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
ISNATLIST(n__cons(n__nil, y0)) → U511(isNat(n__nil), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(57) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(58) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(59) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__zeros) → ISNATLIST(cons(0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(61) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0))

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(63) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(64) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(65) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(cons(n__0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(n__0, n__zeros)), activate(y0))

(66) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))
ISNATLIST(n__cons(n__zeros, y0)) → U511(isNat(n__cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(67) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(68) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(69) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U511(tt, n__zeros) → ISNATLIST(cons(n__0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

(70) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(71) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISNATLIST(n__cons(n__length(x0), y1)) → U511(isNat(length(activate(x0))), activate(y1))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATLIST(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = x1 + x2   
POL(U511(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(72) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))
U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(73) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U511(tt, n__length(x0)) → ISNATLIST(length(activate(x0)))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATLIST(x1)) = x1   
POL(U21(x1)) = x1   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U511(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(74) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(75) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATLIST(n__cons(n__s(x0), y1)) → U511(isNat(s(activate(x0))), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U511(x1, x2) ) = max{0, x1 + x2 - 1}


POL( ISNATLIST(x1) ) = x1


POL( cons(x1, x2) ) = 2x1 + 2x2


POL( s(x1) ) = x1 + 1


POL( U51(x1, x2) ) = max{0, -2}


POL( U61(x1, ..., x3) ) = 2x1


POL( U62(x1, x2) ) = 2


POL( length(x1) ) = 1


POL( U21(x1) ) = 2


POL( isNat(x1) ) = x1 + 1


POL( U52(x1) ) = max{0, 2x1 - 1}


POL( isNatList(x1) ) = max{0, -2}


POL( activate(x1) ) = x1


POL( n__zeros ) = 0


POL( zeros ) = 0


POL( n__0 ) = 0


POL( 0 ) = 0


POL( n__length(x1) ) = 1


POL( n__s(x1) ) = x1 + 1


POL( n__cons(x1, x2) ) = 2x1 + 2x2


POL( n__nil ) = 0


POL( nil ) = 0


POL( tt ) = 1



The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
s(X) → n__s(X)
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil

(76) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(77) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U511(tt, n__s(x0)) → ISNATLIST(s(activate(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U511(x1, x2) ) = 2x2


POL( ISNATLIST(x1) ) = x1


POL( cons(x1, x2) ) = 2x2


POL( s(x1) ) = 1


POL( U51(x1, x2) ) = max{0, x1 - 2}


POL( U61(x1, ..., x3) ) = 2


POL( U62(x1, x2) ) = 2


POL( length(x1) ) = 2x1 + 2


POL( U21(x1) ) = max{0, -2}


POL( isNat(x1) ) = max{0, -2}


POL( U52(x1) ) = max{0, -2}


POL( isNatList(x1) ) = 2x1 + 1


POL( activate(x1) ) = x1


POL( n__zeros ) = 0


POL( zeros ) = 0


POL( n__0 ) = 0


POL( 0 ) = 0


POL( n__length(x1) ) = 2x1 + 2


POL( n__s(x1) ) = 1


POL( n__cons(x1, x2) ) = 2x2


POL( n__nil ) = 0


POL( nil ) = 0


POL( tt ) = 0



The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
0 → n__0
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil

(78) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(79) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATLIST(n__cons(n__cons(x0, x1), y1)) → U511(isNat(cons(activate(x0), x1)), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(U511(x1, x2)) = 0 +
[0,0]
·x1 +
[0,1]
·x2

POL(tt) =
/0\
\0/

POL(n__cons(x1, x2)) =
/1\
\0/
 +
/00\
\10/
·x1 +
/00\
\01/
·x2

POL(ISNATLIST(x1)) = 0 +
[0,1]
·x1

POL(cons(x1, x2)) =
/1\
\0/
 +
/00\
\10/
·x1 +
/00\
\01/
·x2

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(isNat(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(n__zeros) =
/1\
\0/

POL(0) =
/0\
\0/

POL(n__0) =
/0\
\0/

POL(zeros) =
/1\
\0/

POL(n__length(x1)) =
/0\
\1/
 +
/00\
\01/
·x1

POL(length(x1)) =
/0\
\1/
 +
/00\
\01/
·x1

POL(n__s(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(s(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(n__nil) =
/0\
\0/

POL(nil) =
/0\
\0/

POL(U21(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(U61(x1, x2, x3)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\00/
·x3

POL(isNatList(x1)) =
/1\
\0/
 +
/10\
\10/
·x1

POL(U51(x1, x2)) =
/1\
\1/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(U52(x1)) =
/0\
\0/
 +
/00\
\00/
·x1

POL(U62(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
isNat(n__s(V1)) → U21(isNat(activate(V1)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil

(80) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U511(tt, n__cons(x0, x1)) → ISNATLIST(cons(activate(x0), x1))
U511(tt, x0) → ISNATLIST(x0)
ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))
U511(tt, n__zeros) → ISNATLIST(n__cons(0, n__zeros))
ISNATLIST(n__cons(n__0, y0)) → U511(isNat(n__0), activate(y0))
U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(81) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U511(isNat(n__0), activate(n__zeros)) evaluates to t =U511(isNat(n__0), activate(n__zeros))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

U511(isNat(n__0), activate(n__zeros)) → U511(isNat(n__0), n__zeros)
with rule activate(X) → X at position [1] and matcher [X / n__zeros]

U511(isNat(n__0), n__zeros) → U511(tt, n__zeros)
with rule isNat(n__0) → tt at position [0] and matcher [ ]

U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros))
with rule U511(tt, n__zeros) → ISNATLIST(n__cons(n__0, n__zeros)) at position [] and matcher [ ]

ISNATLIST(n__cons(n__0, n__zeros)) → U511(isNat(n__0), activate(n__zeros))
with rule ISNATLIST(n__cons(x0, y1)) → U511(isNat(x0), activate(y1))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(82) NO

(83) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(84) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U611(tt, L, N) → U621(isNat(activate(N)), activate(L))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( LENGTH(x1) ) = 0


POL( U611(x1, ..., x3) ) = max{0, 2x1 - 1}


POL( U621(x1, x2) ) = max{0, -1}


POL( U51(x1, x2) ) = max{0, -2}


POL( U61(x1, ..., x3) ) = x1 + 2


POL( U62(x1, x2) ) = 2


POL( cons(x1, x2) ) = 2


POL( isNatList(x1) ) = max{0, -2}


POL( length(x1) ) = 2


POL( s(x1) ) = 2


POL( isNat(x1) ) = max{0, x1 - 1}


POL( U21(x1) ) = 1


POL( U52(x1) ) = max{0, 2x1 - 1}


POL( activate(x1) ) = x1


POL( n__zeros ) = 0


POL( zeros ) = 1


POL( n__0 ) = 0


POL( 0 ) = 0


POL( n__length(x1) ) = 2


POL( n__s(x1) ) = 2


POL( n__cons(x1, x2) ) = 2


POL( n__nil ) = 1


POL( nil ) = 0


POL( tt ) = 1



The following usable rules [FROCOS05] were oriented:

activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
s(X) → n__s(X)
length(X) → n__length(X)
cons(X1, X2) → n__cons(X1, X2)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))

(85) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U621(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → U611(isNatList(activate(L)), activate(L), N)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U62(tt, L) → s(length(activate(L)))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(86) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(87) TRUE

(88) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, V2) → ISNATILIST(activate(V2))
ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U21(tt) → tt
U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
zeros → n__zeros
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(89) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

U41(tt, V2) → U42(isNatIList(activate(V2)))
U42(tt) → tt
isNatIList(n__cons(V1, V2)) → U41(isNat(activate(V1)), activate(V2))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATILIST(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U411(x1, x2)) = x1 + 2·x2   
POL(U51(x1, x2)) = x1 + 2·x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = 2·x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 1   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(90) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, V2) → ISNATILIST(activate(V2))
ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(91) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, V2) → ISNATILIST(activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(zeros)
U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)

(92) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2))
U411(tt, n__zeros) → ISNATILIST(zeros)
U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(93) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(V1, V2)) → U411(isNat(activate(V1)), activate(V2)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))

(94) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__zeros) → ISNATILIST(zeros)
U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(95) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__zeros) → ISNATILIST(zeros) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(n__zeros)

(96) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__0) → ISNATILIST(0)
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, n__nil) → ISNATILIST(nil)
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(n__zeros)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(97) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(98) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1))
U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(99) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__zeros, y1)) → U411(isNat(zeros), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__zeros), activate(y0))

(100) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__zeros), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(101) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(102) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1))
U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(103) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__0, y1)) → U411(isNat(0), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

(104) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__0) → ISNATILIST(0)
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(105) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__0) → ISNATILIST(0) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__0) → ISNATILIST(n__0)

(106) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__0) → ISNATILIST(n__0)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(107) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(108) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__nil) → ISNATILIST(nil)
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(109) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__nil) → ISNATILIST(nil) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__nil) → ISNATILIST(n__nil)

(110) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__nil) → ISNATILIST(n__nil)

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(111) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(112) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(113) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__nil, y1)) → U411(isNat(nil), activate(y1)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__nil, y0)) → U411(isNat(n__nil), activate(y0))

(114) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
ISNATILIST(n__cons(n__nil, y0)) → U411(isNat(n__nil), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(115) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(116) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(117) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__zeros) → ISNATILIST(cons(0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

(118) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(119) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0))

(120) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(0, n__zeros)), activate(y0))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(121) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(122) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(123) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(cons(n__0, n__zeros)), activate(y0)) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(n__0, n__zeros)), activate(y0))

(124) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))
ISNATILIST(n__cons(n__zeros, y0)) → U411(isNat(n__cons(n__0, n__zeros)), activate(y0))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(125) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(126) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(127) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule U411(tt, n__zeros) → ISNATILIST(cons(n__0, n__zeros)) at position [0] we obtained the following new rules [LPAR04]:

U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

(128) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))
ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(129) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U411(tt, n__length(x0)) → ISNATILIST(length(activate(x0)))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATILIST(x1)) = x1   
POL(U21(x1)) = x1   
POL(U411(x1, x2)) = 2·x1 + 2·x2   
POL(U51(x1, x2)) = 2·x1 + 2·x2   
POL(U52(x1)) = 2·x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(130) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))
U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(131) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

ISNATILIST(n__cons(n__length(x0), y1)) → U411(isNat(length(activate(x0))), activate(y1))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ISNATILIST(x1)) = 2·x1   
POL(U21(x1)) = x1   
POL(U411(x1, x2)) = x1 + 2·x2   
POL(U51(x1, x2)) = x1 + x2   
POL(U52(x1)) = x1   
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3   
POL(U62(x1, x2)) = 1 + x1 + 2·x2   
POL(activate(x1)) = x1   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(isNat(x1)) = 2·x1   
POL(isNatList(x1)) = x1   
POL(length(x1)) = 1 + 2·x1   
POL(n__0) = 0   
POL(n__cons(x1, x2)) = 2·x1 + 2·x2   
POL(n__length(x1)) = 1 + 2·x1   
POL(n__nil) = 0   
POL(n__s(x1)) = x1   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x1)) = x1   
POL(tt) = 0   
POL(zeros) = 0   

(132) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(133) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U411(tt, n__s(x0)) → ISNATILIST(s(activate(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U411(x1, x2) ) = max{0, x1 + 2x2 - 1}


POL( ISNATILIST(x1) ) = x1


POL( cons(x1, x2) ) = 2x2


POL( s(x1) ) = x1 + 1


POL( U51(x1, x2) ) = max{0, -1}


POL( U61(x1, ..., x3) ) = 2x1 + 1


POL( U62(x1, x2) ) = x1 + 2


POL( length(x1) ) = 2


POL( U21(x1) ) = 1


POL( isNat(x1) ) = 1


POL( U52(x1) ) = max{0, 2x1 - 1}


POL( isNatList(x1) ) = max{0, -2}


POL( activate(x1) ) = x1


POL( n__zeros ) = 0


POL( zeros ) = 0


POL( n__0 ) = 0


POL( 0 ) = 0


POL( n__length(x1) ) = 2


POL( n__s(x1) ) = x1 + 1


POL( n__cons(x1, x2) ) = 2x2


POL( n__nil ) = 2


POL( nil ) = 2


POL( tt ) = 1



The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
s(X) → n__s(X)
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil

(134) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(135) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATILIST(n__cons(n__s(x0), y1)) → U411(isNat(s(activate(x0))), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U411(x1, x2) ) = 2x2 + 2


POL( ISNATILIST(x1) ) = 2x1 + 2


POL( cons(x1, x2) ) = 2x1 + 2x2


POL( U51(x1, x2) ) = x1 + 2


POL( U61(x1, ..., x3) ) = 2x2 + 2


POL( U62(x1, x2) ) = 2x2 + 2


POL( length(x1) ) = x1 + 2


POL( s(x1) ) = 2


POL( U21(x1) ) = max{0, -2}


POL( isNat(x1) ) = max{0, -2}


POL( U52(x1) ) = max{0, 2x1 - 2}


POL( isNatList(x1) ) = 2


POL( activate(x1) ) = x1


POL( n__zeros ) = 0


POL( zeros ) = 0


POL( n__0 ) = 0


POL( 0 ) = 0


POL( n__length(x1) ) = x1 + 2


POL( n__s(x1) ) = 2


POL( n__cons(x1, x2) ) = 2x1 + 2x2


POL( n__nil ) = 0


POL( nil ) = 0


POL( tt ) = 0



The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
s(X) → n__s(X)
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
cons(X1, X2) → n__cons(X1, X2)
0 → n__0
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil

(136) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(137) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ISNATILIST(n__cons(n__cons(x0, x1), y1)) → U411(isNat(cons(activate(x0), x1)), activate(y1))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(U411(x1, x2)) = 0 +
[0,0]
·x1 +
[0,1]
·x2

POL(tt) =
/0\
\1/

POL(n__cons(x1, x2)) =
/1\
\0/
 +
/00\
\10/
·x1 +
/00\
\01/
·x2

POL(ISNATILIST(x1)) = 0 +
[0,1]
·x1

POL(cons(x1, x2)) =
/1\
\0/
 +
/00\
\10/
·x1 +
/00\
\01/
·x2

POL(activate(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(isNat(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(n__zeros) =
/1\
\0/

POL(0) =
/0\
\0/

POL(n__0) =
/0\
\0/

POL(zeros) =
/1\
\0/

POL(n__length(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(length(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(n__s(x1)) =
/0\
\1/
 +
/01\
\00/
·x1

POL(s(x1)) =
/0\
\1/
 +
/01\
\00/
·x1

POL(n__nil) =
/0\
\0/

POL(nil) =
/0\
\0/

POL(U21(x1)) =
/0\
\1/
 +
/00\
\00/
·x1

POL(U61(x1, x2, x3)) =
/0\
\0/
 +
/00\
\01/
·x1 +
/00\
\00/
·x2 +
/10\
\00/
·x3

POL(isNatList(x1)) =
/1\
\0/
 +
/00\
\00/
·x1

POL(U51(x1, x2)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(U52(x1)) =
/0\
\0/
 +
/00\
\01/
·x1

POL(U62(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

The following usable rules [FROCOS05] were oriented:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
cons(X1, X2) → n__cons(X1, X2)
isNat(n__s(V1)) → U21(isNat(activate(V1)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U21(tt) → tt
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
zeros → n__zeros
nil → n__nil

(138) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U411(tt, n__cons(x0, x1)) → ISNATILIST(cons(activate(x0), x1))
U411(tt, x0) → ISNATILIST(x0)
ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))
U411(tt, n__zeros) → ISNATILIST(n__cons(0, n__zeros))
ISNATILIST(n__cons(n__0, y0)) → U411(isNat(n__0), activate(y0))
U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))

The TRS R consists of the following rules:

activate(n__zeros) → zeros
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(X) → X
isNat(n__0) → tt
isNat(n__s(V1)) → U21(isNat(activate(V1)))
U21(tt) → tt
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
length(cons(N, L)) → U61(isNatList(activate(L)), activate(L), N)
length(X) → n__length(X)
isNatList(n__cons(V1, V2)) → U51(isNat(activate(V1)), activate(V2))
U61(tt, L, N) → U62(isNat(activate(N)), activate(L))
U62(tt, L) → s(length(activate(L)))
U51(tt, V2) → U52(isNatList(activate(V2)))
U52(tt) → tt
0 → n__0
zeros → cons(0, n__zeros)
zeros → n__zeros

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(139) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U411(isNat(n__0), activate(n__zeros)) evaluates to t =U411(isNat(n__0), activate(n__zeros))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

U411(isNat(n__0), activate(n__zeros)) → U411(isNat(n__0), n__zeros)
with rule activate(X) → X at position [1] and matcher [X / n__zeros]

U411(isNat(n__0), n__zeros) → U411(tt, n__zeros)
with rule isNat(n__0) → tt at position [0] and matcher [ ]

U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros))
with rule U411(tt, n__zeros) → ISNATILIST(n__cons(n__0, n__zeros)) at position [] and matcher [ ]

ISNATILIST(n__cons(n__0, n__zeros)) → U411(isNat(n__0), activate(n__zeros))
with rule ISNATILIST(n__cons(x0, y1)) → U411(isNat(x0), activate(y1))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(140) NO